perm filename SET.A1[1,JRA] blob sn#016812 filedate 1972-12-07 generic text, type T, neo UTF8
00050	
00100	PRE_OP:A,B,U,f,SB;
00200	INF_OP:∩;
00300	INF_PRED:ε,≡,⊂;
00400	VAR: x,y,z,u,v,X,Y,Z,V;
00500	a1:f(x,y)εx ∧ f(x,y)εy ⊃x≡y;
00525	f(SB(A)∩SB(B),SB(A∩B))ε(SB(A)∩SB(B));
00537	
00550	
00600	a2:x≡y ⊃((zεx ⊃ zεy)∧(zεy ⊃ zεx));
00700	a3:(zεx ∧ zεy) ↔zεx∩y;
00900	a5:(z⊂x ∧ z⊂y)↔ z⊂x∩y;
01000	a7:(z⊂x∧zεU) ↔zεSB(x);
01200	;